* fix:  Const initializations  problems dafny-lang#1111 (dafny-lang#1509)

Fixed dafny-lang#1111

* Only emit captureState when debugging with /mv (dafny-lang#1465)

### Changes

- Do not emit `assume {:capturestate ...} true` statements unless the `/mv:<file>` option, which is only used for debugging, is passed. These statements contained source locations which prevent proof isolation.

### Testing

- A side effect of the first change is that source locations in error messages may shift, since previously sometimes the location attached to an `assume {:capturestate ...} true` at the end of a block, which would be the location of any `ensures` clauses, was being picked as the return location of the block. I believe the new behavior is better so I've updated the tests, but please verify.

* Separate document verification from load (dafny-lang#1516)

* Extracted the text change migration into a new service

* Added cancellation token to the position resolution

* Added the possible exceptions to the XML doc.

* Extracted the symbol relocation into a dedicated service

* Removed the default token argument

* Moved document updates to database to make it fully responsible of cancellation

* Added integration tests for OnSave/Never verification status messages

* Made document opening more self-descriptive

* Moved the verification responsibility to the document database

* Removed the SerializedCounterExamples from the document constructor

* Restructured code

* Reduce the TPL stress by mutually exclude verification asynchronously

* Moved verification back to the document loader

* Fixed doc typos

* Now verifying documents on the large stack thread

Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Enhance `Import` printer (dafny-lang#1487)

This commit optimises `Import M = M` to `Import M`, and `Import
M\`{N}` to `Import M\`N`. It also fixes and adds to the existing tests
for module insertion.

Co-authored-by: Hira Syeda <syedahir@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Counterexamples from Command Line (dafny-lang#1511)

* Move position extraction to DafnyModelState

* Move DafnyModel parsing to DafnyModel class

* Add /extractCounterExample option

* Add a lit Test

* Update option description

* Change source location reporting

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

* chore(version): Bump version for pre-release (dafny-lang#1524)

* Bump version for pre-release
* Allow PR title to satisfy semantic PRs app

* chore: Fix version number in attributes (dafny-lang#1525)

* Add document symbols to support outline (dafny-lang#1483)

Enable support for document outlines and the breadcrumb navigation at the top of the editor.

Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* chore: xUnit-based lit test runner (dafny-lang#680)

Adds an xUnit-based test runner for all of the lit tests under Test.

The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite.

Where this alternate runner really shines is in IDEs that support .NET test frameworks:

Getting a tree of test results in the UI
Being able to re-run/debug individual tests by right-clicking on them
Filtering by test name (e.g. dotnet test --filter DisplayName~allocated)
(Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.)

This change adds two new .NET packages:

XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter.
IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory.
Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package.

There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory.

Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged).

Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Update Boogie to 2.9.4 (dafny-lang#1531)

Co-authored-by: Remy Willems <>

* No more `assume 2 < 2;` (dafny-lang#1354)

* Add test file

* Don't remove Lit brackets when assert/assume

By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`.

* Refactor Assert helper methods

This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway.

* Redo changes lost in the merge

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* fix: Document outline for functions and methods without body (dafny-lang#1536)

This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature).

The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1.

Co-authored-by: Remy Willems <rgv.willems@gmail.com>
Co-authored-by: Christoph Amrein <camrein@users.noreply.github.com>
Co-authored-by: hirataqdees <syeda.hira.taqdees@gmail.com>
Co-authored-by: Hira Syeda <syedahir@amazon.com>
Co-authored-by: Aleksandr Fedchin <sasha.fedchin@gmail.com>
Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Rustan Leino <leino@amazon.com>

* fix:  Const initializations  problems #1111 (#1509)

Fixed #1111

* Only emit captureState when debugging with /mv (#1465)

### Changes

- Do not emit `assume {:capturestate ...} true` statements unless the `/mv:<file>` option, which is only used for debugging, is passed. These statements contained source locations which prevent proof isolation.

### Testing

- A side effect of the first change is that source locations in error messages may shift, since previously sometimes the location attached to an `assume {:capturestate ...} true` at the end of a block, which would be the location of any `ensures` clauses, was being picked as the return location of the block. I believe the new behavior is better so I've updated the tests, but please verify.

* Separate document verification from load (#1516)

* Extracted the text change migration into a new service

* Added cancellation token to the position resolution

* Added the possible exceptions to the XML doc.

* Extracted the symbol relocation into a dedicated service

* Removed the default token argument

* Moved document updates to database to make it fully responsible of cancellation

* Added integration tests for OnSave/Never verification status messages

* Made document opening more self-descriptive

* Moved the verification responsibility to the document database

* Removed the SerializedCounterExamples from the document constructor

* Restructured code

* Reduce the TPL stress by mutually exclude verification asynchronously

* Moved verification back to the document loader

* Fixed doc typos

* Now verifying documents on the large stack thread

Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Enhance `Import` printer (#1487)

This commit optimises `Import M = M` to `Import M`, and `Import
M\`{N}` to `Import M\`N`. It also fixes and adds to the existing tests
for module insertion.

Co-authored-by: Hira Syeda <syedahir@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Counterexamples from Command Line (#1511)

* Move position extraction to DafnyModelState

* Move DafnyModel parsing to DafnyModel class

* Add /extractCounterExample option

* Add a lit Test

* Update option description

* Change source location reporting

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

* chore(version): Bump version for pre-release (#1524)

* Bump version for pre-release
* Allow PR title to satisfy semantic PRs app

* chore: Fix version number in attributes (#1525)

* Add document symbols to support outline (#1483)

Enable support for document outlines and the breadcrumb navigation at the top of the editor.

Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* chore: xUnit-based lit test runner (#680)

Adds an xUnit-based test runner for all of the lit tests under Test.

The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite.

Where this alternate runner really shines is in IDEs that support .NET test frameworks:

Getting a tree of test results in the UI
Being able to re-run/debug individual tests by right-clicking on them
Filtering by test name (e.g. dotnet test --filter DisplayName~allocated)
(Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.)

This change adds two new .NET packages:

XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter.
IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory.
Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package.

There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory.

Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged).

Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Update Boogie to 2.9.4 (#1531)

Co-authored-by: Remy Willems <>

* No more `assume 2 < 2;` (#1354)

* Add test file

* Don't remove Lit brackets when assert/assume

By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`.

* Refactor Assert helper methods

This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway.

* Redo changes lost in the merge

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* fix: Document outline for functions and methods without body (#1536)

This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature).

The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1.

Co-authored-by: Remy Willems <rgv.willems@gmail.com>
Co-authored-by: Christoph Amrein <camrein@users.noreply.github.com>
Co-authored-by: hirataqdees <syeda.hira.taqdees@gmail.com>
Co-authored-by: Hira Syeda <syedahir@amazon.com>
Co-authored-by: Aleksandr Fedchin <sasha.fedchin@gmail.com>
Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Rustan Leino <leino@amazon.com>

* fix:  Const initializations  problems #1111 (#1509)

Fixed #1111

* Only emit captureState when debugging with /mv (#1465)

- Do not emit `assume {:capturestate ...} true` statements unless the `/mv:<file>` option, which is only used for debugging, is passed. These statements contained source locations which prevent proof isolation.

- A side effect of the first change is that source locations in error messages may shift, since previously sometimes the location attached to an `assume {:capturestate ...} true` at the end of a block, which would be the location of any `ensures` clauses, was being picked as the return location of the block. I believe the new behavior is better so I've updated the tests, but please verify.

* Separate document verification from load (#1516)

* Extracted the text change migration into a new service

* Added cancellation token to the position resolution

* Added the possible exceptions to the XML doc.

* Extracted the symbol relocation into a dedicated service

* Removed the default token argument

* Moved document updates to database to make it fully responsible of cancellation

* Added integration tests for OnSave/Never verification status messages

* Made document opening more self-descriptive

* Moved the verification responsibility to the document database

* Removed the SerializedCounterExamples from the document constructor

* Restructured code

* Reduce the TPL stress by mutually exclude verification asynchronously

* Moved verification back to the document loader

* Fixed doc typos

* Now verifying documents on the large stack thread

Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Enhance `Import` printer (#1487)

This commit optimises `Import M = M` to `Import M`, and `Import
M\`{N}` to `Import M\`N`. It also fixes and adds to the existing tests
for module insertion.

Co-authored-by: Hira Syeda <syedahir@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Counterexamples from Command Line (#1511)

* Move position extraction to DafnyModelState

* Move DafnyModel parsing to DafnyModel class

* Add /extractCounterExample option

* Add a lit Test

* Update option description

* Change source location reporting

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

* chore(version): Bump version for pre-release (#1524)

* Bump version for pre-release
* Allow PR title to satisfy semantic PRs app

* chore: Fix version number in attributes (#1525)

* Add document symbols to support outline (#1483)

Enable support for document outlines and the breadcrumb navigation at the top of the editor.

Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* chore: xUnit-based lit test runner (#680)

Adds an xUnit-based test runner for all of the lit tests under Test.

The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite.

Where this alternate runner really shines is in IDEs that support .NET test frameworks:

Getting a tree of test results in the UI
Being able to re-run/debug individual tests by right-clicking on them
Filtering by test name (e.g. dotnet test --filter DisplayName~allocated)
(Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.)

This change adds two new .NET packages:

XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter.
IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory.
Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package.

There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory.

Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged).

Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Update Boogie to 2.9.4 (#1531)

Co-authored-by: Remy Willems <>

* No more `assume 2 < 2;` (#1354)

* Add test file

* Don't remove Lit brackets when assert/assume

By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`.

* Refactor Assert helper methods

This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway.

* Redo changes lost in the merge

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* fix: Document outline for functions and methods without body (#1536)

This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature).

The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1.

Co-authored-by: Remy Willems <rgv.willems@gmail.com>
Co-authored-by: Christoph Amrein <camrein@users.noreply.github.com>
Co-authored-by: hirataqdees <syeda.hira.taqdees@gmail.com>
Co-authored-by: Hira Syeda <syedahir@amazon.com>
Co-authored-by: Aleksandr Fedchin <sasha.fedchin@gmail.com>
Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Rustan Leino <leino@amazon.com>

* fix:  Const initializations  problems #1111 (#1509)

Fixed #1111

* Only emit captureState when debugging with /mv (#1465)

- Do not emit `assume {:capturestate ...} true` statements unless the `/mv:<file>` option, which is only used for debugging, is passed. These statements contained source locations which prevent proof isolation.

- A side effect of the first change is that source locations in error messages may shift, since previously sometimes the location attached to an `assume {:capturestate ...} true` at the end of a block, which would be the location of any `ensures` clauses, was being picked as the return location of the block. I believe the new behavior is better so I've updated the tests, but please verify.

* Separate document verification from load (#1516)

* Extracted the text change migration into a new service

* Added cancellation token to the position resolution

* Added the possible exceptions to the XML doc.

* Extracted the symbol relocation into a dedicated service

* Removed the default token argument

* Moved document updates to database to make it fully responsible of cancellation

* Added integration tests for OnSave/Never verification status messages

* Made document opening more self-descriptive

* Moved the verification responsibility to the document database

* Removed the SerializedCounterExamples from the document constructor

* Restructured code

* Reduce the TPL stress by mutually exclude verification asynchronously

* Moved verification back to the document loader

* Fixed doc typos

* Now verifying documents on the large stack thread

Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Enhance `Import` printer (#1487)

This commit optimises `Import M = M` to `Import M`, and `Import
M\`{N}` to `Import M\`N`. It also fixes and adds to the existing tests
for module insertion.

Co-authored-by: Hira Syeda <syedahir@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Counterexamples from Command Line (#1511)

* Move position extraction to DafnyModelState

* Move DafnyModel parsing to DafnyModel class

* Add /extractCounterExample option

* Add a lit Test

* Update option description

* Change source location reporting

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

* chore(version): Bump version for pre-release (#1524)

* Bump version for pre-release
* Allow PR title to satisfy semantic PRs app

* chore: Fix version number in attributes (#1525)

* Add document symbols to support outline (#1483)

Enable support for document outlines and the breadcrumb navigation at the top of the editor.

Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* chore: xUnit-based lit test runner (#680)

Adds an xUnit-based test runner for all of the lit tests under Test.

The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite.

Where this alternate runner really shines is in IDEs that support .NET test frameworks:

Getting a tree of test results in the UI
Being able to re-run/debug individual tests by right-clicking on them
Filtering by test name (e.g. dotnet test --filter DisplayName~allocated)
(Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.)

This change adds two new .NET packages:

XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter.
IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory.
Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package.

There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory.

Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged).

Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Update Boogie to 2.9.4 (#1531)

Co-authored-by: Remy Willems <>

* No more `assume 2 < 2;` (#1354)

* Add test file

* Don't remove Lit brackets when assert/assume

By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`.

* Refactor Assert helper methods

This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway.

* Redo changes lost in the merge

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* fix: Document outline for functions and methods without body (#1536)

This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature).

The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1.

Co-authored-by: Remy Willems <rgv.willems@gmail.com>
Co-authored-by: Christoph Amrein <camrein@users.noreply.github.com>
Co-authored-by: hirataqdees <syeda.hira.taqdees@gmail.com>
Co-authored-by: Hira Syeda <syedahir@amazon.com>
Co-authored-by: Aleksandr Fedchin <sasha.fedchin@gmail.com>
Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Rustan Leino <leino@amazon.com>

* fix:  Const initializations  problems dafny-lang#1111 (dafny-lang#1509)

Fixed dafny-lang#1111

* Only emit captureState when debugging with /mv (dafny-lang#1465)

### Changes

- Do not emit `assume {:capturestate ...} true` statements unless the `/mv:<file>` option, which is only used for debugging, is passed. These statements contained source locations which prevent proof isolation.

### Testing

- A side effect of the first change is that source locations in error messages may shift, since previously sometimes the location attached to an `assume {:capturestate ...} true` at the end of a block, which would be the location of any `ensures` clauses, was being picked as the return location of the block. I believe the new behavior is better so I've updated the tests, but please verify.

* Separate document verification from load (dafny-lang#1516)

* Extracted the text change migration into a new service

* Added cancellation token to the position resolution

* Added the possible exceptions to the XML doc.

* Extracted the symbol relocation into a dedicated service

* Removed the default token argument

* Moved document updates to database to make it fully responsible of cancellation

* Added integration tests for OnSave/Never verification status messages

* Made document opening more self-descriptive

* Moved the verification responsibility to the document database

* Removed the SerializedCounterExamples from the document constructor

* Restructured code

* Reduce the TPL stress by mutually exclude verification asynchronously

* Moved verification back to the document loader

* Fixed doc typos

* Now verifying documents on the large stack thread

Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Enhance `Import` printer (dafny-lang#1487)

This commit optimises `Import M = M` to `Import M`, and `Import
M\`{N}` to `Import M\`N`. It also fixes and adds to the existing tests
for module insertion.

Co-authored-by: Hira Syeda <syedahir@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Counterexamples from Command Line (dafny-lang#1511)

* Move position extraction to DafnyModelState

* Move DafnyModel parsing to DafnyModel class

* Add /extractCounterExample option

* Add a lit Test

* Update option description

* Change source location reporting

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

* chore(version): Bump version for pre-release (dafny-lang#1524)

* Bump version for pre-release
* Allow PR title to satisfy semantic PRs app

* chore: Fix version number in attributes (dafny-lang#1525)

* Add document symbols to support outline (dafny-lang#1483)

Enable support for document outlines and the breadcrumb navigation at the top of the editor.

Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* chore: xUnit-based lit test runner (dafny-lang#680)

Adds an xUnit-based test runner for all of the lit tests under Test.

The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite.

Where this alternate runner really shines is in IDEs that support .NET test frameworks:

Getting a tree of test results in the UI
Being able to re-run/debug individual tests by right-clicking on them
Filtering by test name (e.g. dotnet test --filter DisplayName~allocated)
(Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.)

This change adds two new .NET packages:

XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter.
IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory.
Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package.

There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory.

Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged).

Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* Update Boogie to 2.9.4 (dafny-lang#1531)

Co-authored-by: Remy Willems <>

* No more `assume 2 < 2;` (dafny-lang#1354)

* Add test file

* Don't remove Lit brackets when assert/assume

By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`.

* Refactor Assert helper methods

This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway.

* Redo changes lost in the merge

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

* fix: Document outline for functions and methods without body (dafny-lang#1536)

This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature).

The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1.

Co-authored-by: Remy Willems <rgv.willems@gmail.com>
Co-authored-by: Christoph Amrein <camrein@users.noreply.github.com>
Co-authored-by: hirataqdees <syeda.hira.taqdees@gmail.com>
Co-authored-by: Hira Syeda <syedahir@amazon.com>
Co-authored-by: Aleksandr Fedchin <sasha.fedchin@gmail.com>
Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Rustan Leino <leino@amazon.com>